T:Type, l1, l2:T List. no_repeats(T;l1 @ l2)  l_disjoint(T;l1;l2) 

latex

Definitions	A & B, x:A. B(x), P & Q, (x  l), t  T, x:A. B(x), Prop, P  Q, A, ||as||, False, AB, , l[i], as @ bs, l_disjoint(T;l1;l2), no_repeats(T;l), ij, i  j < k, {i..j}, P  Q, P  Q, True, T
Lemmas	select append back, squash wf, select append front, le wf, length append, non neg length, length wf1, append wf, nat wf, not wf, select wf, l member wf